$\forall$$T$:Type, ${\it dT}$:EqDecider($T$), $L$:$T$ List, $x$, $y$:$T$.
\\[0ex]($x$ $\in$ $L$) $\Rightarrow$ ($y$ $\in$ $L$) $\Rightarrow$ index($L$;$x$)$\leq$index($L$;$y$) $\Rightarrow$ $x$ before $y$ $\in$ $L$ $\vee$ $x$ $=$ $y$